rev(ls) → r1(ls, empty)
r1(empty, a) → a
r1(cons(x, k), a) → r1(k, cons(x, a))
↳ QTRS
↳ DependencyPairsProof
rev(ls) → r1(ls, empty)
r1(empty, a) → a
r1(cons(x, k), a) → r1(k, cons(x, a))
R1(cons(x, k), a) → R1(k, cons(x, a))
REV(ls) → R1(ls, empty)
rev(ls) → r1(ls, empty)
r1(empty, a) → a
r1(cons(x, k), a) → r1(k, cons(x, a))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
R1(cons(x, k), a) → R1(k, cons(x, a))
REV(ls) → R1(ls, empty)
rev(ls) → r1(ls, empty)
r1(empty, a) → a
r1(cons(x, k), a) → r1(k, cons(x, a))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
R1(cons(x, k), a) → R1(k, cons(x, a))
rev(ls) → r1(ls, empty)
r1(empty, a) → a
r1(cons(x, k), a) → r1(k, cons(x, a))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
R1(cons(x, k), a) → R1(k, cons(x, a))
The value of delta used in the strict ordering is 11.
POL(cons(x1, x2)) = 4 + x_2
POL(R1(x1, x2)) = (4)x_1 + (5/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
rev(ls) → r1(ls, empty)
r1(empty, a) → a
r1(cons(x, k), a) → r1(k, cons(x, a))